Nuprl Lemma : fifo-antecedent-order-preserving 13,45

es:ES, Sys:AbsInterface(Top), f:sys-antecedent(es;Sys).
fifo-antecedent(es;Sys;f)
 (ab:E(Sys).
 (loc(a) = loc(b Id)
  (loc(f(a)) = loc(f(b))  Id)
  {(f(a) <loc f(b))  (a <loc b)}) 
latex


Upabstract chain replication
Definitionsfifo-antecedent(es;Sys;f), s = t, t  T, x:AB(x), x:AB(x), EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(Epred?info), kindcase(ka.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,yt(x;y), <ab>, A, pred(e), first(e), xt(x), P & Q, Top, ES, E(X), E, AbsInterface(A), e c e', {x:AB(x)} , sys-antecedent(es;Sys), P  Q, e loc e' , let x,y = A in B(x;y), t.1, loc(e), Atom$n, {T}, (e <loc e'), False, (e < e'), P  Q, (x  l), P  Q, X(e), e(e1,e2].P(e), @e(xv), (last change to x before e), A c B, pred(e), e  X, f(x)?z
Lemmassingleton-subtype, es-is-interface wf, es-E-interface-strong-subtype, es-causl irreflexivity, iff wf, rev implies wf, es-causl wf, es-locl transitivity2, es-le weakening eq, es-locl irreflexivity, es-locl wf, es-le-total, event system wf, es-interface wf, fifo-antecedent wf, sys-antecedent wf, es-E-interface-subtype rel, es-loc wf, es-causle wf, es-E wf, es-E-interface wf, deq wf, EOrderAxioms wf, IdLnk wf, Msg wf, unit wf, nat wf, val-axiom wf, qle wf, cless wf, bool wf, top wf, Knd wf, kindcase wf, constant function wf, assert wf, not wf, loc wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf

origin